Nuprl Lemma : l_disjoint_intersection 11,40
T:Type, eq:EqDecider(T), a, b, c:(T List).
(l_disjoint(T;b;a)  l_disjoint(T;c;a))  l_disjoint(T;l_intersection(eq;b;c);a) 
latex

DefinitionsP & Q, x:A. B(x), t  T, False, P  Q, A, Void, left + right, P  Q, (x  l), x:A  B(x), x:AB(x), P  Q, P  Q, l_disjoint(T;l1;l2), type List, EqDecider(T), Type,
Lemmasnot functionality wrt iff, and functionality wrt iff, member-intersection

origin